ABSTRACT In this paper we present a new semantic approach for propositional linear temporal logic with discrete time, strongly based in the well-order of IN (the set of natural numbers). We consider temporal connectives which express precedence, posteriority and simultaneity, and they provide a family of expressively complete temporal logics. The selection of the new semantics and connectives used in this work was principally to obtain a suitable executable temporal logic, which can be used for the specification and control of (...) process behaviour in discrete time in a similar way to thai presented by D. Gabbay in [GAB 89], Our new approach has two advantages: firstly, the connectives are defined intuitively so that they have interpretations which relate to properties of interest in real systems; secondly, it provides a new semantics that facilitates simpler proofs of many valid formulas and metatheorems. To confirm this second advantage, we use our semantics to give a formal proof of the Separation Theorem for one of these logics (specifically LN3). The great interest of this Separation Theorem for the executable temporal logic is emphasised by D. Gabbay in [GAB 89], [GAB 88]. (shrink)

ABSTRACT Most theorem provers for Classical Logic transform the input formula into a particular normal form. This tranformation is done before the execution of the algorithm or it is integrated into the deductive algorithm. This situation is no different for Non-Classical Logics and, particularly, for Temporal Logics. However, unlike classical logic, temporal logic does not provide an extension of the notion of non negative normal form. In this work, we define a temporal negative normal form for the future fragment of (...) the linear time propositional temporal logic, named FNext. The definition saves as much information as possible about implicants and implicates of the input formula and its subformulas. This property is the novelty of this normal form; for example, in [Fis97] the normal form is guided by the separation property and in [Ven86] the normal form provided prepares the input formula to be treated by a resolution method. Moreover, we also introduce an algorithm having linear cost, which transforms the input formula into a temporal negative normal form. Furthermore, in this work we present a new structure and a set of operators over it that allows us to efficiently manage the information about unitary implicants and implicates contained in the subformulae. (shrink)

This book constitutes the refereed proceedings of the European Workshop on Logics in Artificial Intelligence, JELIA 2000, held in Malaga, Spain in September/October 2000. The 24 revised full papers presented together with three invited papers were carefully reviewed and selected out of 60 submissions. The papers are organized in topical sections on knowledge representation, reasoning about actions, belief revision, theorem proving, argumentation, agents, decidability and complexity, updates, and preferences.